package edu.gatech.cc.concolic;

import gov.nasa.jpf.Config;
import gov.nasa.jpf.JPF;
import gov.nasa.jpf.jvm.NoUncaughtExceptionsProperty;
import gov.nasa.jpf.search.Simulation;

public class Concolic {

	native public static int makeSymbolic(int i);
	native public static char makeSymbolic(char c);
	native public static String makeSymbolic(String s);
	
	public static String CONCOLIC_EXECUTION_STRATEGY = "concolic.strategy";
	public static ExecutionStrategy executionStrategy;
	
	public static void main(String[] args) {
		
		Config config = JPF.createConfig(args);
		config.setProperty("search.class", Simulation.class.getName());
		config.setProperty("jpf.report.console.start", "");
		config.setProperty("jpf.report.console.finished", "");
		config.setProperty("search.properties", NoUncaughtExceptionsProperty.class.getName());
		config.setProperty("vm.storage.class", "");
		config.setProperty("vm.peer.packages", Concolic.class.getPackage().getName() + ",<model>,gov.nasa.jpf.jvm,<default>");
		config.setProperty("vm.insn_factory.class", ConcolicInstructionFactory.class.getName());
		
		try {
			executionStrategy = config.getInstance(CONCOLIC_EXECUTION_STRATEGY, ExecutionStrategy.class);
		} catch (Exception e) {
		}
		
		if(null == executionStrategy) {
			executionStrategy = new DefaultExecutionStrategy(config);
		}
		
		JPF jpf = new JPF(config);
		jpf.run();
		
		executionStrategy.exit();
	}
}
